\begin{tabbing}
ecl{-}add{-}catch($A$;$l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$ = $A$ in \+
\\[0ex]$\langle$${\it Ta}$
\\[0ex]$,\,$${\it ksa}$
\\[0ex]$,\,$${\it ia}$
\\[0ex]$,\,$${\it ga}$
\\[0ex]$,\,$(\=$\lambda$$n$,$x$. $\neg_{2}$deq{-}member(NatDeq;$n$;$l$) $\wedge_{2}$ ${\it ha}$($n$,$x$)\+
\\[0ex]$\vee_{2}$ $n$=$_{2}$0 $\wedge_{2}$ reduce($\lambda$$m$,$b$. ${\it ha}$($m$,$x$) $\vee_{2}$ $b$;false$_{2}$;$l$))
\-\\[0ex]$,\,$${\it aa}$
\\[0ex]$,\,$list{-}diff(NatDeq;${\it ea}$;$l$)$\rangle$
\-
\end{tabbing}